<html><body>You can repeat the next editor command any number of times
by pressing <b>C+ENTER</b>, followed by the desired repeat count.
</body></html>
